Research efforts at universities, as well as new-product offerings from design tool vendors, are constantly seeking ways to raise design productivity in the face of increasing complexity. With verification taking up to 70 percent of design time, this is a critical area of focus in the time-to-market battle. No wonder, then, that interest in verification techniques is on an upswing, as the number of paper submissions on the subject for this year's Design Automation Conference (DAC) attests. While general paper-submission growth year over year from 2001 was 19 percent, the number of papers submitted on the topic of verification grew by 28 percent.
Many new and upgraded verification tools work within existing design frameworks and use existing design specification languages. In concert with simulation, they take on the challenge of proving design correctness. However, increasing complexity has many in the design community looking beyond these traditional methods to advances that can drastically improve productivity, notably formal verification.
Formal verification is the application of rigorous mathematical techniques to prove the functional equivalence of an electronic design with its original specification. A collective term that refers to a number of tools and methodologies, formal verification is used to verify a design's functional behavior.
Recent efforts in formal verification have focused on moving beyond comparing combinational logic to determining equivalence of sequential behavior, or the satisfaction of certain sequential properties, even if the sequential parts of the two circuits are not in direct correspondence. Advances in formal verification techniques such as bounded model checking, the integration of verification into the design process at the point of concept and new verification-based languages like ForSpec are some of the most promising examples.
Compared with pure model-checking techniques, which must explore the entire design state space, bounded model-checking (BMC) explores a limited portion of the state space. BMC is useful in determining bugs that are exercised in the part of the state space explored.
Integrating verification into the design process at the point of concept is also a hot area. Designers can potentially save valuable time by using the same language for design specification as for simulation, formal verification and synthesis. Such languages provide additional features in the form of assertions that must be true for a design.
In contrast, completely new verification-based languages like ForSpec, which have a foundation in mathematically rigorous temporal logic, are being proposed. While such languages give designers a huge boost in verification confidence, they also are a move away from traditional languages and design description styles.
The debate over formal verification will be explored in depth at DAC in June. A panel of experts will discuss getting around the brick wall of complexity that surrounds formal techniques.
The basic question is just how much of a methodology change will be needed to successfully integrate formal verification into the design process. Panelists represent each position on the spectrum-from those who believe that formal methods can be handled just by advances in verification methodology, necessitating no changes in design flow, to advocates for an entirely new language and methodology.
It is up in the air at the moment which new verification techniques designers will embrace. What is certain is that if any are to be successful, there is a need for standards and further educational opportunities so the industry can keep up with the increasing challenges of electronics design.
---
Sharad Malik (malik@princeton.edu) is panel chair for the 2002 Design Automation Conference, to be held June 10-14 in New Orleans. He is a professor in Princeton University's EE department (Princeton, N.J.).
http://www.isdmag.com
Copyright © 2002 CMP Media LLC
4/1/02, Issue # 14154, page 46.
